A, B:Type, L2:((tg:Id  (AB(Top List))) List), L:((:Top  (:Id  Top)) List), tg:Id, a:A, b:B.
{(map(x.x.2;L) = concat(map(tgf.map(x.<tgf.1, x>;(tgf.2)(a,b));L2))  ((tg:Id  Top) List))
 ((tg  map(p.p.1;L2)))
 (filter(ms.(ms.2).1 = tg;L) = []  ((:Top  (:Id  Top)) List))} 

latex

Definitions	x:A. B(x), {T}, , concat(ll), map(f;as), P  Q, P & Q, P  Q, filter(P;l), a = b, t.1, t.2, x. t(x), t  T, (x  l), Id, Top, x:A. B(x), A, P  Q, False
Lemmas	l member wf, pi2 wf, pi1 wf, eq id wf, filter wf, nil-iff-no-member, top wf, Id wf, map wf, concat wf, not wf, member filter, assert-eq-id, member map, member-concat